0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 0 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 4 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 0 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇔, 1 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇔, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
hC_in_g(c(s(T8), T9)) → U3_g(T8, T9, fA_in_gg(T8, T9))
fA_in_gg(s(T18), T19) → U1_gg(T18, T19, fA_in_gg(T18, s(T19)))
U1_gg(T18, T19, fA_out_gg(T18, s(T19))) → fA_out_gg(s(T18), T19)
U3_g(T8, T9, fA_out_gg(T8, T9)) → hC_out_g(c(s(T8), T9))
U3_g(T8, T9, fA_out_gg(T8, T9)) → U4_g(T8, T9, gB_in_gg(T8, T9))
gB_in_gg(T28, s(T29)) → U2_gg(T28, T29, gB_in_gg(s(T28), T29))
U2_gg(T28, T29, gB_out_gg(s(T28), T29)) → gB_out_gg(T28, s(T29))
U4_g(T8, T9, gB_out_gg(T8, T9)) → hC_out_g(c(s(T8), T9))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
hC_in_g(c(s(T8), T9)) → U3_g(T8, T9, fA_in_gg(T8, T9))
fA_in_gg(s(T18), T19) → U1_gg(T18, T19, fA_in_gg(T18, s(T19)))
U1_gg(T18, T19, fA_out_gg(T18, s(T19))) → fA_out_gg(s(T18), T19)
U3_g(T8, T9, fA_out_gg(T8, T9)) → hC_out_g(c(s(T8), T9))
U3_g(T8, T9, fA_out_gg(T8, T9)) → U4_g(T8, T9, gB_in_gg(T8, T9))
gB_in_gg(T28, s(T29)) → U2_gg(T28, T29, gB_in_gg(s(T28), T29))
U2_gg(T28, T29, gB_out_gg(s(T28), T29)) → gB_out_gg(T28, s(T29))
U4_g(T8, T9, gB_out_gg(T8, T9)) → hC_out_g(c(s(T8), T9))
HC_IN_G(c(s(T8), T9)) → U3_G(T8, T9, fA_in_gg(T8, T9))
HC_IN_G(c(s(T8), T9)) → FA_IN_GG(T8, T9)
FA_IN_GG(s(T18), T19) → U1_GG(T18, T19, fA_in_gg(T18, s(T19)))
FA_IN_GG(s(T18), T19) → FA_IN_GG(T18, s(T19))
U3_G(T8, T9, fA_out_gg(T8, T9)) → U4_G(T8, T9, gB_in_gg(T8, T9))
U3_G(T8, T9, fA_out_gg(T8, T9)) → GB_IN_GG(T8, T9)
GB_IN_GG(T28, s(T29)) → U2_GG(T28, T29, gB_in_gg(s(T28), T29))
GB_IN_GG(T28, s(T29)) → GB_IN_GG(s(T28), T29)
hC_in_g(c(s(T8), T9)) → U3_g(T8, T9, fA_in_gg(T8, T9))
fA_in_gg(s(T18), T19) → U1_gg(T18, T19, fA_in_gg(T18, s(T19)))
U1_gg(T18, T19, fA_out_gg(T18, s(T19))) → fA_out_gg(s(T18), T19)
U3_g(T8, T9, fA_out_gg(T8, T9)) → hC_out_g(c(s(T8), T9))
U3_g(T8, T9, fA_out_gg(T8, T9)) → U4_g(T8, T9, gB_in_gg(T8, T9))
gB_in_gg(T28, s(T29)) → U2_gg(T28, T29, gB_in_gg(s(T28), T29))
U2_gg(T28, T29, gB_out_gg(s(T28), T29)) → gB_out_gg(T28, s(T29))
U4_g(T8, T9, gB_out_gg(T8, T9)) → hC_out_g(c(s(T8), T9))
HC_IN_G(c(s(T8), T9)) → U3_G(T8, T9, fA_in_gg(T8, T9))
HC_IN_G(c(s(T8), T9)) → FA_IN_GG(T8, T9)
FA_IN_GG(s(T18), T19) → U1_GG(T18, T19, fA_in_gg(T18, s(T19)))
FA_IN_GG(s(T18), T19) → FA_IN_GG(T18, s(T19))
U3_G(T8, T9, fA_out_gg(T8, T9)) → U4_G(T8, T9, gB_in_gg(T8, T9))
U3_G(T8, T9, fA_out_gg(T8, T9)) → GB_IN_GG(T8, T9)
GB_IN_GG(T28, s(T29)) → U2_GG(T28, T29, gB_in_gg(s(T28), T29))
GB_IN_GG(T28, s(T29)) → GB_IN_GG(s(T28), T29)
hC_in_g(c(s(T8), T9)) → U3_g(T8, T9, fA_in_gg(T8, T9))
fA_in_gg(s(T18), T19) → U1_gg(T18, T19, fA_in_gg(T18, s(T19)))
U1_gg(T18, T19, fA_out_gg(T18, s(T19))) → fA_out_gg(s(T18), T19)
U3_g(T8, T9, fA_out_gg(T8, T9)) → hC_out_g(c(s(T8), T9))
U3_g(T8, T9, fA_out_gg(T8, T9)) → U4_g(T8, T9, gB_in_gg(T8, T9))
gB_in_gg(T28, s(T29)) → U2_gg(T28, T29, gB_in_gg(s(T28), T29))
U2_gg(T28, T29, gB_out_gg(s(T28), T29)) → gB_out_gg(T28, s(T29))
U4_g(T8, T9, gB_out_gg(T8, T9)) → hC_out_g(c(s(T8), T9))
GB_IN_GG(T28, s(T29)) → GB_IN_GG(s(T28), T29)
hC_in_g(c(s(T8), T9)) → U3_g(T8, T9, fA_in_gg(T8, T9))
fA_in_gg(s(T18), T19) → U1_gg(T18, T19, fA_in_gg(T18, s(T19)))
U1_gg(T18, T19, fA_out_gg(T18, s(T19))) → fA_out_gg(s(T18), T19)
U3_g(T8, T9, fA_out_gg(T8, T9)) → hC_out_g(c(s(T8), T9))
U3_g(T8, T9, fA_out_gg(T8, T9)) → U4_g(T8, T9, gB_in_gg(T8, T9))
gB_in_gg(T28, s(T29)) → U2_gg(T28, T29, gB_in_gg(s(T28), T29))
U2_gg(T28, T29, gB_out_gg(s(T28), T29)) → gB_out_gg(T28, s(T29))
U4_g(T8, T9, gB_out_gg(T8, T9)) → hC_out_g(c(s(T8), T9))
GB_IN_GG(T28, s(T29)) → GB_IN_GG(s(T28), T29)
GB_IN_GG(T28, s(T29)) → GB_IN_GG(s(T28), T29)
From the DPs we obtained the following set of size-change graphs:
FA_IN_GG(s(T18), T19) → FA_IN_GG(T18, s(T19))
hC_in_g(c(s(T8), T9)) → U3_g(T8, T9, fA_in_gg(T8, T9))
fA_in_gg(s(T18), T19) → U1_gg(T18, T19, fA_in_gg(T18, s(T19)))
U1_gg(T18, T19, fA_out_gg(T18, s(T19))) → fA_out_gg(s(T18), T19)
U3_g(T8, T9, fA_out_gg(T8, T9)) → hC_out_g(c(s(T8), T9))
U3_g(T8, T9, fA_out_gg(T8, T9)) → U4_g(T8, T9, gB_in_gg(T8, T9))
gB_in_gg(T28, s(T29)) → U2_gg(T28, T29, gB_in_gg(s(T28), T29))
U2_gg(T28, T29, gB_out_gg(s(T28), T29)) → gB_out_gg(T28, s(T29))
U4_g(T8, T9, gB_out_gg(T8, T9)) → hC_out_g(c(s(T8), T9))
FA_IN_GG(s(T18), T19) → FA_IN_GG(T18, s(T19))
FA_IN_GG(s(T18), T19) → FA_IN_GG(T18, s(T19))
From the DPs we obtained the following set of size-change graphs: